$\forall$$b$:$\mathbb{B}$, $A$:Type, $p$,$q$:$A$. if $b$ then $p$ else $q$ fi $\in$ $A$